(declare-const v0 Bool)
(declare-const v3 Bool)
(declare-const v7 Bool)
(declare-const i3 Int)
(declare-const i6 Int)
(declare-fun st2 () (Set Int))
(declare-fun st3 () (Set Int))
(declare-fun st5 () (Set Int))
(declare-fun st7 () (Set Int))
(declare-fun st11 () (Set Int))
(declare-fun st13 () (Set Int))
(declare-const i21 Int)
(declare-const i23 Int)
(declare-const i25 Int)
(declare-const v12 Bool)
(assert (> (card st3) (ite (=> v7 v3) 46 1960)))
(declare-const v14 Bool)
(declare-const v19 Bool)
(declare-const v22 Bool)
(declare-const v27 Bool)
(assert (and (or v19 (= i21 i3) (not v0)) (or v22 (>= 53 i23 76) v12) (or (member (mod i6 46) st7) v27 (subset (union st5 (intersection st11 st2)) st5)) (or (member i25 st13) v22 (>= 53 i23 76)) (or (subset (union st5 (intersection st11 st2)) st5) v14 v12) (or v27 (subset (union st5 (intersection st11 st2)) st5) v22) (or v12 v12 (>= 53 i23 76))))
(check-sat)
